Nuprl Lemma : mon_itop_split 13,42

g:IMonoid, abc:.
(a  b)
 (b  c)
 (E:({a..c}|g|).
 ( a  j < cE(j)) = (( a  j < bE(j)) * ( b  j < cE(j)))  |g|) 
latex


Upgroups 1
Definitions of Statement lb  i < ubE(i)
Definitions lb  i < ubE(i)
Lemmasitop split

origin